doc.posFromIndex(this._validLead),

        doc.posFromIndex(totalLength - this._validTrail));

      this._retrievedText =

        this._retrievedText.slice(0, this._validLead) +

        mid +

        this._retrievedText.slice(this._retrievedText.length - this._validTrail);

      this._validLead = -1;

​

      return this._retrievedText;

    }

​

    private _docChanges(docChanges: CodeMirror.EditorChange[]) {

​

      var doc = this.textDoc.doc;

​

      var lineCount = doc.lineCount();

      var newTotalLength = doc.indexFromPos({

        line: lineCount - 1,

        ch: doc.getLine(lineCount - 1).length

      });

​

      var changeLead = -1;

      var changeTrail = -1;

      var deltaLength = 0;

      for (var i = 0; i < docChanges.length; i++) {

        var ch = docChanges[i];

        var removedLength = totalLength(ch.removed);

        var addedLength = totalLength(ch.text);

        var fromIndex = doc.indexFromPos(ch.from);

        var trail = newTotalLength - fromIndex - addedLength;

        deltaLength += addedLength - removedLength;

        if (changeLead < 0) {

          changeLead = fromIndex;

          changeTrail = trail;

        }

        else {

          changeLead = Math.min(changeLead, fromIndex);

          changeTrail = Math.min(changeTrail, trail);

        }

      }

      if (this._validLead < 0) {

        this._validLead = changeLead;

        this._validTrail = changeTrail;

      }

      else {

        this._validLead = Math.min(this._validLead, changeLead);

        this._validTrail = Math.min(this._validTrail, changeTrail);

      }

​

      var changeSummary = {

        lead: changeLead,

        mid: this._totalLength - changeLead - changeTrail,

        newmid: 0,

        trail: changeTrail

      };

      changeSummary.newmid = changeSummary.mid + deltaLength;

      if (this.textDoc.onChanges) {

        this.textDoc.onChanges(docChanges, changeSummary);

      }

​

      this._totalLength = newTotalLength;

​

      if (this._scrollerModel)

        this._scrollerModel.docChanges(docChanges);

​

      this._saveTimer.interval = (this.moduleObj && this.moduleObj.saveDelay) || saveDelay;

      this._saveTimer.reset();

​